Step of Proof: nth_tl_is_fseg 11,40
Inference at * 1 1 
Iof proof for Lemma nth tl is fseg:



1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. L2 = (L @ L1)
  L1 = nth_tl(||L||;L @ L1) 
latex
 by ThinVar `L2' 
latex

 1: 

 1: 3. L : T List
 1:   L1 = nth_tl(||L||;L @ L1)
 .

origin